User blog:Emlightened/System Tau Notes
I'm really really sorry, but this is incomplete. I have been making a text document (up to 42kb rn) trying to formalise and explain a Googological System, but it was never finished. I've not edited it in two months, and thought it was a better idea to let it die here than on my hard drive. Still, I'm pretty sure there are some interesting and salvageable ideas here. Since writing it, I've learned a lot of type theory (in particular, I think I have a decent understanding of inductive-recursive types), so if I come back here at some point, I should be able to clean up the presentation and present what I have in an inductive, not recursive, manner. (I'd probably also switch from math notation to computing notation, too. Easier to work with in practice.) The basic idea is to create some recursive types (like labelled binary trees, lists, etc.), and to bestow well-founded orderings onto them, so they can be used for recursion in the way googologists normally do. That said, here it is: ##~~## = Incomplete section = Ramble/comment = System \(\tau\) = Introducing System \(\tau\) (tau). \(\tau\) is a googological system (a system designed specifically for the verification of googological notations as total recursive) based on a first order type theory. It is geared towards notations that are based on ordinal-like structures, not seperator-based structures, although the latter can be encoded with some difficulty. There are four sorts of object: terms (which are used to represent expressions), (data) types, functions, and orderings (used to show a function with recursion halts). Motivation The motivation for a googological system in general is clear: we have a formal system that can prove that notations actually work as expected (although not necessarily how strong they are), so this section deals with why \(\tau\) was designed as it is. One of the main issues with making a system in general is probably encoding the data types. Googologists regularly create complex data types for their notations, so any system should be able to encode most or all of these. My solution is to note that most data types can be represented as either a choice between terms of (possibly) different data types (sum) or pair of terms of (possibly) different data types (product). For illustration: *A natural is a choice between 0 and the successor of a natural. *A list of X is a choice between the empty list or a pair of a list of X and an X. *A binary tree is a choice between the empty tree or a pair of two binary trees. Hence, we describe data types using inductive types, and formailse these through unit, sum, product and recursive types. Other than that, we need to formalise functions, which means formalising lots of recursion. To do this, when defining a function, we allow self-reference. To avoid infinite loops, we further require that whenever f(x) contains reference to f(a), some a, we can prove a a_1 > a_2 > \cdots \).) We define this collection below. For operations on orderings, instead of using the normal curly brackets (parentheses, \(()\)) for clarification or precidence, we use square brackets \(\,\). This is simply for clearness, the square brackets are not operations in themselves. Sum and Product Orderings Given types \(A\) and \(B\) with orderings \(<^A\) and \(<^B\) we can define the sum orderings \(<^A+<^B\), \(<^A\overset{\leftarrow}+<^B\) and \(<^A+\overset{\to}<^B\), and the product orderings \(<^A\times<^B\), \(<^A\overset{\leftarrow}\times<^B\) and \(<^A\overset{\to}\times<^B\) as follows: * Let \(a:A\), \(a':A\), \(b:B\) and \(b':B\) with \(a<^Aa'\) and \(b<^Bb'\). *If \(a<^Aa'\), \(La <^A+<^B La'\) and if \(b<^Bb'\), \(Rb <^A+<^B Rb'\) *If \(a<^Aa'\), \((a,b) <^A\times<^B (a',b)\) and if \(b<^Bb'\), \((a,b) <^A\times<^B (a,b')\) *\(Rb <^A\overset{\leftarrow}+<^B La\) and \(La <^A\overset{\to}+<^B Rb\) *If \(c:A\times B\), \(c':A\times B\) and \(c <^A\times<^B c'\), \(c <^A\overset{\leftarrow}\times<^B c'\) and \(c <^A\overset{\to}\times<^B c'\) \(<^A\overset{\leftarrow}\times<^B\) and \(<^A\overset{\to}\times<^B\) are weakened lexicographic orders which are specified in the subsection after next. Embedding Orderings Embedding orderings are fairly simple. Simply put, if \(<^A:A\) and \(a:\mu\alpha.A\) is a subterm of \(a':\mu\alpha.A\), then \(a \mu<^\alpha.<^A a'\). Also, if \(a <^A[<^\alpha:=\mu<^\alpha.<^A] a'\), then \(a \mu<^\alpha.<^A a'\). Additionally, some conditions have to be met before making an embedding ordering, to preserve strictness. For instance, in \(\mu\alpha.\mathbf 1+\alpha\), we can't start with \(<^1\overset{\leftarrow}+<^\alpha\) as then \(Lu>RLu\), and we would ahve to have \(Lu<:(N×α)α=μα.1+N×α embedding order product order When looking at ordering stuff of type X, ordering stuff of sub-type Y, and have X #} μα.A #} Y #} α (with #} meaning 'contains as a substring'), have the condition that the type-α term at the bottom is smaller than 0 00 000 0000 1 01 001 0001 10 010 0010 100 0100 1000 11 Our types are equivalent to simultaneously inducttive types. In particular, a specification of the form: Ax = Ax \n Ax Ax = Var := SoP SoP = 0 SoP = P SoP = SoP|SoP P = 1 P = Var P = P&P can represent an arbitary family of simultaneous inductive types, and also is equivalent to a recursive type. Also, do same for corecursive? ##~~## --> Examples of functions Proof of encoding Primitive Recursion Consider \(F:D \to A\) and \(G: \texttt{Nat} \times A \times D \to A\). \(\lambda Hb:\texttt{Nat} \times D \to A.(\lambda:L\texttt{Nat} \times D\to A.F\pi_2 b)\oplus\lambda:R\texttt{Nat} \times D\to A.GH(\delta_2^\texttt{Nat}\pi_1b,\pi_2b)\) This isn't the most elegant way of presenting our function. Let's represent it in a more understandable way: *\(H(Rn,d) = G(n,H(n),d)\) *\(H(0,d) = F(d)\) That's the function definitions taken care of, however we still need to prove the function is valid, by supplying the appropiate ordering \(<:\texttt{Nat} \times D\) for which \((\delta_2^\texttt{Nat}\pi_1b,\pi_2b) < b\) when \(b:R\texttt{Nat} \times D\). As it turns out, the standard ordering on \(\texttt{Nat} \times D\) is sufficient. Proof of encoding Ackermann Function The definition for the Ackermann function \(A:\texttt{Nat}^2 \to \texttt{Nat}\) is: *(\(S:\texttt{Nat} \to \texttt{Nat} = R\) and \(P:\mathbf 0 + \texttt{Nat} \to \texttt{Nat} = \delta_2\) are successor and predecessor.) *\(A(0,n) = Sn\) *\(A(Sn,0) = A(n,1)\) *\(A(Sn,Sm) = A(n,A(Sn,m))\) *So, as a \(\lambda\) expression: \(\lambda At:\texttt{Nat}^2 \to \texttt{Nat}.(\lambda: (\mathbf 1 + \mathbf 0) \times \texttt{Nat}.S\pi_2 t)\uplus(\lambda: (\mathbf 0 + \texttt{Nat}) \times (\mathbf 1 + \mathbf 0) \to \texttt{Nat}.A(P\pi_1t,1))\uplus(\lambda:(\mathbf 0 + \texttt{Nat})^2 \to \texttt{Nat}.A(P\pi_1t,A(\pi_1t,P\pi_2t)))\) Hrm. As you can tell, the \(\lambda\) expression doesn't really make anything any clearer. We'll only write them out explicitly when it either shows the function works as expected, or makes things clearer. Anyway, here we require an \(<:\texttt{Nat}^2\) so \((n,1) < (Rn,0)\), \((n,A(Rn,m)) < (Rn,Rm)\) and \((Rn,m) < (Rn,Rm)\). Either \(A\) is decreasing according to \(<\) (false), or we can simplify the second of these to \((n,x) < (Rn,Rm)\), arbitary \(x\), which suggests we order by the first component, then the second (lexicographic order). Multi-variable Ackermann Function Defintion: *An = n+1 *An+1, 0 = An, 1 *Aa+1, n+1 = Aa, A[\cdots, a+1, n] *Aa+1, 0, \cdots_0, n = Aa, n, \cdots_0, n Hrm. Don't really like that \(A0, 0 = 1\), but whatever, it's the only version with a wiki page. Anyway, this is the point where we need to use the concept of a decreasing function (not just smaller subterm), and where case distinction can't just be realised at the type level. This is because we are defining a single \(A\) function that works on any length list, not a \(A\) function for each length. ##~~## Wainer Hierarchy ##~~## ########20:24, November 3, 2017 (UTC)~εmli######## END POST HEREISH Presenting a notation in \(\tau\) Make a new blag post for this? And leave until after \(\tau l\) and \(\tau\varepsilon\)? >>> Give a schema sufficient for defining data structures and functions of many notations in \(\tau\), maintaining compatibility with the orderings that exist whenever possible. >>> Give a list of simple functinos which can simply be stated as in \(\tau\) but are a bit more difficult to represent directly, and how to use the result (as it may return an encoded (as product) curried function). >>> Have a bunch of methods that are still \(\tau\) but a lot easier to use than \(\tau\) directly. Basically syntactic sugar. = Extenions = This section will be periodically added to with various extensions. Hopefully, it will be fully up to date. Summaries Theory complete? new types new orderings summary \(\tau\varepsilon\) 0% no yes, on \(\mu\alpha.A\) \(\tau l\) 0% yes yes \(\tau\to\) 0% closure under \(\to\) ? \(\tau2^-\) 0% so closure under \(\forall\) no \(\tau\mathcal B\) 0% fo closure under \(\nu\) no? Theory: % Done: Adds: \(\tau\varepsilon\) 0% More embedding-based orderings \(\tau l\) 0% Miscelleneous types and orderings \(\tau\to\) 0% Arrow types, and recursive types without negation fixed points \(\tau2^-\) 0% Polytypes (universal quantification over function types) \(\tau\mathcal B\) 0% Corecursive types and bar recursion Embedding Orderings: \(\tau\varepsilon\) This is easily the most useful extension currently planned. It allows weakenings of the embedding ordering to be made, which in turn allows for ordinal collapsing functions to be encoded, greatly boosting the system. Miscelleneous Types and Orders: \(\tau l\) This extension is in part syntactic sugar. It adds many new basic types and orderings designed so that the system becomes more intuitive to use and so that the encoding is less extrenuous. Higher Order: \(\tau\to\) This extension closes the system under arrow types. It is a simple extension that allows function exponentiation, and function-to-function transformations in general (functionals) to be described. It also allows recursive types to be applied to arrow types in ways that preserve normalisation and the existence of empty types. # \(\alpha \in \alpha\) # \(\alpha \in A\) implies \(\alpha \in D\) where \(D\) is \(A+B\), \(B+A\), \(A \times B\), or \(B \times A\) # \(\alpha \in A\) or \(-\alpha \in B\) implies \(\alpha \in A \to B\) # \(\alpha = --\alpha\) # \(\mu\alpha.A\) can only be done if \(-\alpha \notin A\) Polytypes: \(\tau2^-\) This extension adds polytypes, which allow universal quantification over function types. It doesn't increase the power of the theory, but does increase flexibility, by allowing creation of (for instance) a length-of function for lists of arbitary type, types for \(L\) and \(R\), and doesn't require type arguments (hence increasing syntactic flexibility). However, this extension is arguably of little practical value, as interest is typically in functions on fixed types. Corecursive: \(\tau\mathcal B\) This extension adds corecursive types to the mix. These types enable us to encode some functions into first-order objects, encode real numbers, and use bar recursion. Notably, although bar recursion prevents us from using the full function space (when the domain type is corecursive, at least), we are able to have the type of real numbers encoded as a corecursive type, allowing proof of the recursiveness and totality of some functions \(f:\mathbb R \to \mathbb R\) # Bar Recursion: # \(\mathcal N = \mu\alpha.1 + \alpha\); \(\mathcal L = \mu\alpha.1 + \mathcal N \times \alpha\); \(\mathcal S = \mu\alpha.\mathcal N \times \alpha\) # Source type fixed(?) to \(\mathcal N\), unfortunately # Given \(Y: \mathcal S \to \mathcal N\), \(G: \mathcal L \to B\), \(H: \mathcal L \times \nu\alpha.B\times\alpha \to B\), produces \(\mathcal BY,G,H: \mathcal L \to B\) # Has following reduction rules: \(\mathcal BY,G,H(a) = G(a)\text{ if }Y(lstr(a)) < len(a)\); \(\mathcal BY,G,H(a) = H(a,fstrn.\mathcal B[Y,G,H(R(n,a))) \text{ otherwise}\) # Where lstr takes a list, reverses it, and returns a stream infinitely extending the result with zeroes, and fstr is the canonical transformation \((\mathcal N \to \mathcal N) \to \mathcal S\) Category:Blog posts